package arlab.formulae.tests
import arlab.formulae._
import arlab.formulae.transformations._

import arlab.picosat2._


object Poject {
    def main (args: Array[String]) ={

      val a = Not(Globally(BooleanVariable("b").&&(BooleanVariable("a"))))
      println("normal:")
      println(a)
      println("nnf:")
      println(Transformations.nnf(a))

      val b = Not(Until(Not(BooleanVariable("b")), Not(BooleanVariable("a"))))
      println("normal:")
      println(b)
      println("nnf:")
      println(Transformations.nnf(b))


      var m = Map():Map[Int, List[BooleanVariable]]
      m=m.updated(0, List(BooleanVariable("b"),BooleanVariable("c")))
      m=m.updated(1, List(BooleanVariable("c")))
      m=m.updated(2, List(BooleanVariable("d")) )

      val krip = Kripke(List(0,1,2), List((0,1),(1,2)), List(0,1,2),m,List(BooleanVariable("b"),BooleanVariable("c"),BooleanVariable("d")))
      println("normal:")
      println(krip.labels)
      println("initCode")
      println(krip.init(0))
      println("transitions:")
      println(krip.step(0,0))
      
      
      var m2 = Map():Map[Int, List[BooleanVariable]]
      m2=m2.updated(0,List())
      m2=m2.updated(1,List(BooleanVariable("z")))
      m2=m2.updated(2,List(BooleanVariable("y")))
      m2=m2.updated(3,List(BooleanVariable("y"),BooleanVariable("z")))
      m2=m2.updated(4,List(BooleanVariable("x")))
      m2=m2.updated(5,List(BooleanVariable("x"),BooleanVariable("z")))
      m2=m2.updated(6,List(BooleanVariable("x"),BooleanVariable("y")))
      m2=m2.updated(7,List(BooleanVariable("x"),BooleanVariable("y"),BooleanVariable("z")))
      
      val krip_schieberegister_Richtig = Kripke(List(0,1,2,3,4,5,6,7), List((0,0), (1,0), (2,1), (3,1), (4,2),(5,2),(6,3),(7,3)),
                                                List(0,1,2,3,4,5,6,7),m2,
                                                List(BooleanVariable("x"),BooleanVariable("y"),BooleanVariable("z")))
      
      
      val krip_schieberegister_Falsch = Kripke(List(0,1,2,3,4,5,6,7), List((0,4),(1,4),(2,5),(3,5),(4,6),(5,6),(6,7),(7,7)),
                                                List(0,1,2,3,4,5,6,7),m2,
                                                List(BooleanVariable("x"),BooleanVariable("y"),BooleanVariable("z")))
      
      
      
      val schieberegister_Falsch = And(And(BooleanVariable("x1").implic(BooleanVariable("y0")),
                                           BooleanVariable("y1").implic(BooleanVariable("z0"))),
                                       BooleanVariable("z1").implic(True))
                                      
      
      val schieberegister_Richtig = And(And(BooleanVariable("x1").implic(BooleanVariable("y0")),
                                            BooleanVariable("y1").implic(BooleanVariable("z0"))),
                                        BooleanVariable("z1").implic(False))   
                                        
      val LTL = Finally(Transformations.simplify(And(And(BooleanVariable("x").implic(False),BooleanVariable("y").implic(False)),
                            BooleanVariable("z").implic(False)))       )    
      
      val LTL2 = Globally(And(And(Not(BooleanVariable("x")), Not(BooleanVariable("y"))), Not(BooleanVariable("z")))) 
      
      val LTL3 = Globally(Or(Or(BooleanVariable("x"), BooleanVariable("y")), BooleanVariable("z")))                                           
                                        
                                        
  //    println(Transformations.boundModelLTL(krip_schieberegister_Falsch,LTL,2)) 
  //    println(krip_schieberegister_Falsch.init(0))     
                                        
                                        
      println("should be true:")                                  
      println(Transformations.boundModelLTL(krip_schieberegister_Richtig,LTL,2)) 
      println("should be false:")                                              
      println(Transformations.boundModelLTL(krip_schieberegister_Falsch,LTL,2)) 
      
      println()
      println(Transformations.boundModelLTL(krip_schieberegister_Falsch,And(And(BooleanVariable("g"),BooleanVariable("f")), 
                                                                            And(Not(BooleanVariable("g")),BooleanVariable("f"))),3))  
      println()             
      println(Transformations.nnf(LTL))                                                         
      println(LTL)                                                                  
      println(LTL2)        
      println(Transformations.nnf(LTL2))
      println(LTL3)
      println(Transformations.nnf(LTL3))
      println(Transformations.LTL_To_Boolean_Loop(LTL, 1, 0, 3))
      println(Transformations.LTL_To_Boolean_Loop(LTL2,1, 2, 3))      
      println(Transformations.LTL_To_Boolean_Loop(LTL3,1, 0, 3))     
      
      
      
      
      println(Transformations.boundModelLTL(krip_schieberegister_Richtig,LTL3,2)) 
      println(Transformations.boundModelLTL(krip_schieberegister_Falsch,LTL3,2))     
      
      println()
      println(krip_schieberegister_Falsch.step(0,1))
      println()
      println(krip_schieberegister_Falsch.init(0))                                                                                                                 
    }
    
}
